$\forall$$T$:Type, $f$:($T$$\rightarrow$$T$), $x$, $y$:$T$. $x$ is $f$$\ast$($y$) $\Rightarrow$ ($\neg$($x$ = $y$)) $\Rightarrow$ $x$ is $f$$\ast$($f$($y$))